Nuprl Lemma : f2f+ReqDcdr_wf 11,40
es:ES, ff:FIFO, f2f+:F2F+-decls. req_dcdr  e:EDec(is_req  (e)) 
latex

Definitionst.2, t.1, req_dcdr, is_req  , t  T, x:A. B(x), F2F+-decls
Lemmasevent system wf, FIFO wf, F2F+-decls wf

origin